%{
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdarg.h>
#include "y.tab.h"
	
void lexEcho(char *format, ...);
%}

unsigned_integer		[a-zA-Z]
general_function		[a-zA-Z]
dollar_dollar_word		[a-zA-Z]
single_quoted			[a-zA-Z]
real				[a-zA-Z]
integer				[a-zA-Z]
dollar_word			[a-zA-Z]
lower_word			[a-zA-Z]
upper_word			[a-zA-Z]
rational			[a-zA-Z]
distinct_object			[a-zA-Z]

%%

"|"				{lexEcho("[|]");
					return VLINE;
}
"*"				{lexEcho("[*]");
					return STAR;
}
"+"				{lexEcho("[+]");
					return PLUS;
}
"!" 				{lexEcho("[!]");
					return FOR_ALL;
}
"?" 				{lexEcho("[?]");
					return THERE_EXISTS;
}
"~" 				{lexEcho("[~]");
					return NOT;
}
"&"				{lexEcho("[&]");
					return AND;
}
"<=>" 				{lexEcho("[<=>]");
					return DOUBLE_ARROW;
}
"=>"				{lexEcho("[=>]");
					return RIGHT_ARROW;
}
"<="				{lexEcho("[<=]");
					return LEFT_ARROW;
}
"<~>"				{lexEcho("[<~>]");
					return XOR;
}
"~|" 				{lexEcho("[~|]");
					return NOR;
}
"~&"				{lexEcho("[~&]");
					return NAND;
}
"="				{lexEcho("[=]");
					return EQUAL_SIGN;
}
"!="				{lexEcho("[!=]");
					return NOT_EQUAL_SIGN;
}
">"				{lexEcho("[>]");
					return ARROW;
}
"-->"				{lexEcho("[-->]");
					return GENTZEN_ARROW;
}
":="				{lexEcho("[:=]");
					return ASSIGN;
}
"^"				{lexEcho("[^]");
					return SYMBOL1;
}
"!>"				{lexEcho("[!>]");
					return SYMBOL2;
}
"?*"				{lexEcho("[?*]");
					return SYMBOL3;
}
"!!"				{lexEcho("[!]");
					return SYMBOL4;
}
"??"				{lexEcho("[??]");
					return SYMBOL5;
}
"thf"				{lexEcho("[thf]");
					return THF;
}
"fof"				{lexEcho("[fof]");
					return FOF;
}
"cnf"				{lexEcho("[cnf]");
					return CNF;
}
"axiom"				{lexEcho("[axiom]");
					return AXIOM;
}
"hypothesis"			{lexEcho("[hypothesis]");
					return HYPOTHESIS;
}
"definition"			{lexEcho("[definition]");
					return DEFINITION;
}
"assumption"			{lexEcho("[assumption]");
					return ASSUMPTION;
}
"lemma"				{lexEcho("[lemma]");
					return LEMMA;
}
"theorem"			{lexEcho("[theorem]");
					return THEOREM;
}
"conjecture"			{lexEcho("[conjecture]");
					return CONJECTURE;
}
"negated_conjecture"		{lexEcho("[negated_conjecture]");
					return NEGATED_CONJECTURE;
}
"plain"				{lexEcho("[plain]");
					return PLAIN;
}
"fi_domain"			{lexEcho("[fi_domain]");
					return FI_DOMAIN;
}
"fi_functors"			{lexEcho("[fi_functors]");
					return FI_FUNCTORS;
}
"fi_predicates"			{lexEcho("[fi_predicates]");
					return FI_PREDICATES;
}
"type"				{lexEcho("[type]");
					return TYPE;
}
"unknown"			{lexEcho("[unknown]");
					return UNKNOWN;
}
"$oType" 			{lexEcho("[$oType]");
					return DOLLAR_OTYPE;
}
"$o"				{lexEcho("[$o]");
					return DOLLAR_O;
}
"$iType"			{lexEcho("[$iType]");
					return DOLLAR_ITYPE;
}
"$i"				{lexEcho("[$i]");
					return DOLLAR_I;
}
"$tType"			{lexEcho("[$tType]");
					return DOLLAR_TTYPE;
}
"$real"				{lexEcho("[$real]");
					return DOLLAR_REAL;
}
"$rat"				{lexEcho("[$rat]");
					return DOLLAR_RAT;
}
"$int"				{lexEcho("[$int]");
					return DOLLAR_INT;
}
"$true"				{lexEcho("[$true]");
					return DOLLAR_TRUE;
}
"$false"			{lexEcho("[$false]");
					return DOLLAR_FALSE;
}
"$equal"			{lexEcho("[$equal]");
					return DOLLAR_EQUAL;
}
"inference"			{lexEcho("[inference]");
					return INFERENCE;
}
"introduced"			{lexEcho("[introduced]");
					return INTRODUCED;
}
"axiom_of_choice"		{lexEcho("[axiom_of_choice]");
					return AXIOM_OF_CHOICE;
}
"tautology"			{lexEcho("[tautology]");
					return TAUTOLOGY;
}
"theory"			{lexEcho("[theory]");
					return THEORY;
}
"equality"			{lexEcho("[equality]");
					return EQUALITY;
}
"ac"				{lexEcho("[ac]");
					return AC;
}
"creator"			{lexEcho("[creator]");
					return CREATOR;
}
"description"			{lexEcho("[description]");
					return DESCRIPTION;
}
"iquote"			{lexEcho("[iquote]");
					return IQUOTE;
}
"status"			{lexEcho("[status]");
					return STATUS;
}
"suc"				{lexEcho("[suc]");
					return SUC;
}
"unp"				{lexEcho("[unp]");
					return UNP;
}
"sap"				{lexEcho("[sap]");
					return SAP;
}
"esa"				{lexEcho("[esa]");
					return ESA;
}
"sat"				{lexEcho("[sat]");
					return SAT;
}
"fsa"				{lexEcho("[fsa]");
					return FSA;
}
"thm"				{lexEcho("[thm]");
					return THM;
}
"eqv"				{lexEcho("[eqv]");
					return EQV;
}
"tac"				{lexEcho("[tac]");
					return TAC;
}
"wec"				{lexEcho("[wec]");
					return WEC;
}
"eth"				{lexEcho("[eth]");
					return ETH;
}
"tau"				{lexEcho("[tau]");
					return TAU;
}
"wtc"				{lexEcho("[wtc]");
					return WTC;
}
"wth"				{lexEcho("[wth]");
					return WTH;
}
"cax"				{lexEcho("[cax]");
					return CAX;
}
"sca"				{lexEcho("[sca]");
					return SCA;
}
"tca"				{lexEcho("[tca]");
					return TCA;
}
"wca"				{lexEcho("[wca]");
					return WCA;
}
"cup"				{lexEcho("[cup]");
					return CUP;
}
"csp"				{lexEcho("[csp]");
					return CSP;
}
"ecs"				{lexEcho("[ecs]");
					return ECS;
}
"csa"				{lexEcho("[csa]");
					return CSA;
}
"cth"				{lexEcho("[cth]");
					return CTH;
}
"ceq"				{lexEcho("[ceq]");
					return CEQ;
}
"unc"				{lexEcho("[unc]");
					return UNC;
}
"wcc"				{lexEcho("[wcc]");
					return WCC;
}
"ect"				{lexEcho("[ect]");
					return ECT;
}
"fun"				{lexEcho("[fun]");
					return FUN;
}
"uns"				{lexEcho("[uns]");
					return UNS;
}
"wuc"				{lexEcho("[wuc]");
					return WUC;
}
"wct"				{lexEcho("[wct]");
					return WCT;
}
"scc"				{lexEcho("[scc]");
					return SCC;
}
"uca"				{lexEcho("[uca]");
					return UCA;
}
"noc"				{lexEcho("[noc]");
					return NOC;
}
"assumptions"			{lexEcho("[assumptions]");
					return ASSUMPTIONS;
}
"refutation"			{lexEcho("[refutation]");
					return REFUTATION;
}
"include"			{lexEcho("[include]");
					return INCLUDE;
}
"$thf"				{lexEcho("[$thf]");
					return DOLLAR_THF;
}
"$fof"				{lexEcho("[$fof]");
					return DOLLAR_FOF;
}
"$cnf"				{lexEcho("[$cnf]");
					return DOLLAR_CNF;
}
"$fot"				{lexEcho("[$fot]");
					return DOLLAR_FOT;
}

%%

void lexEcho(char *format, ...) {
	va_list args;
	
	#ifdef LEX_DEBUG
		va_start(args, format);
		vfprintf(stderr, format, args);
		va_end(args);
	#endif
}
